[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification classnamefuns
enrich classname with
   predicates 
       . l< . : classname × classname;
      comment: lexicographical order on class names,
                                         needed only for actualizations. Has nothing to
                                         do with the class hierarchy.;
       
       . <_1 . : classname × classname;
      comment: c1 <_1 c2 ↔ class c1 extends c2.;
       
       . ≤ . : classname × classname;
      comment: encodes class hierarchy. Has only two axioms,
                                         le-one and transitivity that define a reflexive partial order
                                         with top element Object.;
       
   
   axioms 
      le-one
      : ⊦ 
        class1 ≤ class2 ↔ class2 = `java.lang.Object' .class ∨ class1 = class2 ∨ class1 <_1 class2 ∨ (∃ class3. class1 <_1 class3 ∧ class3 ≤ class2);
      comment: the generation mechanism for axioms for ≤ will ensure that the
                  class hierarchy is always wellformed.;
       
      le-transitive :  ⊦ class1 ≤ class2 ∧ class2 ≤ class3 → class1 ≤ class3;
      comment: cannot be proved from the other axiom, but is very useful.;
      used for : f, lf;
       
      less-def :  ⊦ str1 .class l< str2 .class ↔ str1 < str2;
      used for : s, ls;
       
      Irreflexivity :  ⊦ ¬ class l< class;
      comment: needed for actualizations;
      used for : s, ls;
       
      Transitivity :  ⊦ class1 l< class2 ∧ class2 l< class3 → class1 l< class3;
      comment: needed for actualizations;
      used for : f, lf;
       
      Totality :  ⊦ class1 l< class2 ∨ class1 = class2 ∨ class2 l< class1;
      comment: needed for actualizations;
       
end enrich